/* ###
 * IP: GHIDRA
 *
 * Licensed under the Apache License, Version 2.0 (the "License");
 * you may not use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *      http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.
 */
package ghidra.pcode.emu.symz3;

import org.apache.commons.lang3.tuple.Pair;

import com.microsoft.z3.BoolExpr;
import com.microsoft.z3.Context;

import ghidra.pcode.emu.DefaultPcodeThread.PcodeThreadExecutor;
import ghidra.pcode.exec.*;
import ghidra.pcode.exec.PcodeArithmetic.Purpose;
import ghidra.program.model.pcode.PcodeOp;
import ghidra.program.model.pcode.Varnode;
import ghidra.symz3.model.SymValueZ3;

/**
 * An instrumented executor for the Symbolic Summarizer
 * 
 * <p>
 * This part is responsible for executing all the actual p-code operations generated by each decoded
 * instruction. Each thread in the emulator gets a distinct executor. So far, we haven't actually
 * added any instrumentation, but the conditions of {@link PcodeOp#CBRANCH} operations will likely
 * be examined by the user, so we set up the skeleton here.
 */
public class SymZ3PcodeThreadExecutor extends PcodeThreadExecutor<Pair<byte[], SymValueZ3>> {
	/**
	 * Create the executor
	 * 
	 * @param thread the thread being created
	 */
	public SymZ3PcodeThreadExecutor(SymZ3PcodeThread thread) {
		super(thread);
	}

	@Override
	public SymZ3PcodeThread getThread() {
		return (SymZ3PcodeThread) super.getThread();
	}

	@Override
	public void stepOp(PcodeOp op, PcodeFrame frame,
			PcodeUseropLibrary<Pair<byte[], SymValueZ3>> library) {
		getThread().addOp(op);
		super.stepOp(op, frame, library);
	}

	/**
	 * {@inheritDoc}
	 * 
	 * <p>
	 * This is invoked on every {@link PcodeOp#CBRANCH}, allowing us a decent place to instrument
	 * the emulator and add preconditions to the symbolic state, as we follow along concretely.
	 * Refer to {@link PcodeExecutor#executeConditionalBranch(PcodeOp, PcodeFrame)} to see the
	 * operations inputs.
	 */
	@Override
	public void executeConditionalBranch(PcodeOp op, PcodeFrame frame) {
		Varnode condVar = op.getInput(1);
		Pair<byte[], SymValueZ3> cond = state.getVar(condVar, reason);
		try (Context ctx = new Context()) {
			BoolExpr symCond = cond.getRight().getBoolExpr(ctx);
			/**
			 * The decision is driven by the concrete (left) side of the emulator, but we should
			 * still figure the equivalent precondition for the symbolic (right) side.
			 */
			if (arithmetic.isTrue(cond, Purpose.CONDITION)) {
				getThread().addPrecondition(SymValueZ3.serialize(ctx, symCond));
			}
			else {
				getThread().addPrecondition(SymValueZ3.serialize(ctx, ctx.mkNot(symCond)));
			}
		}
		super.executeConditionalBranch(op, frame);
	}
}
